module models/examples/tutorial/filesystem

// File system objects
abstract sig FSObject {}
sig File, Dir extends FSObject {}

// A File System
sig FileSystem {
  root: Dir,
  objects: set FSObject,
  contents: Dir lone-> FSObject,
  parent: FSObject ->lone Dir
}{
  // root has no parent
  no root.parent
  // objects are those reachable from the root
  objects = root.*contents
  // contents only defined on objects
  contents in objects->objects
  // parent is the inverse of contents
  parent = ~contents
}

// Move FSObject f to Directory d
pred mv (fs, fs': FileSystem, f: FSObject, d: Dir) {
  (f + d) in fs.objects
  fs'.contents = fs.contents - f.(fs.parent)->f + d->f
}

assert moveWorks {
    all fs, fs': FileSystem, f: FSObject, d:Dir | 
      mv(fs, fs', f, d) =>  (fs.root = fs'.root && fs.objects = fs'.objects)
  }

check moveWorks for 15
 
// Delete the file f
pred rm (fs, fs': FileSystem, f: File) {
  f in fs.objects
  fs'.contents = fs.contents - f.(fs.parent)->f
}

pred delete (fs, fs': FileSystem, f: FSObject) {
	f in fs.(objects - root)
	no f.(fs.contents)
	fs'.contents = fs.contents - f.(fs.parent)->f
     no fs'.contents => fs'.root = fs.root // new constraint
}

assert deleteWorks {
    all fs, fs': FileSystem, f: FSObject  |
      delete(fs, fs', f) =>
        (fs.root = fs'.root && fs.objects - f = fs'.objects)
  }

check deleteWorks for 2

// Delete the directory d
pred rmdir(fs, fs': FileSystem, d: Dir) {
  d in fs.(objects - root)
  no d.(fs.contents) //d is empty
  fs'.contents = fs.contents - d.(fs.parent)->d
}

// Recursively delete the file system object f
pred rm_r(fs, fs': FileSystem, f: FSObject) {
  f in fs.(objects - root)
  let subtree = f.*(fs.contents) |
    fs'.contents = fs.contents - subtree.(fs.parent)->subtree
}

run mv for 2 FileSystem, 4 FSObject
run rm for 2 FileSystem, 4 FSObject
run rmdir for 2 FileSystem, 4 FSObject
run rm_r for 2 FileSystem, 4 FSObject


// Moving doesn't add or delete any file system objects
assert moveAddsRemovesNone {
  all fs, fs': FileSystem, f: FSObject, d:Dir |
    mv(fs, fs', f, d) => fs.objects = fs'.objects
}

// rm removes exactly the specified file
assert rmRemovesOneFile {
  all fs, fs': FileSystem, f: File |
    rm(fs, fs', f) => fs.objects - f = fs'.objects
}

// rmdir removes exactly the specified directory
assert rmdirRemovesOneDir {
  all fs, fs': FileSystem, d: Dir |
    rmdir(fs, fs', d) => fs.objects - d = fs'.objects
}

// rm_r removes exactly the specified subtree
assert rm_rRemovesSubtree {
  all fs, fs': FileSystem, f: FSObject |
    rm_r(fs, fs', f) => fs.objects - f.*(fs.contents) = fs'.objects
}

// rm and rm_r same effect on files
assert rmAndrm_rSameForFiles {
  all fs, fs1, fs2: FileSystem, f: File |
    rm(fs, fs1, f) && rm_r(fs, fs2, f) => fs1.contents = fs2.contents
}

check moveAddsRemovesNone for 5 //passes
check rmRemovesOneFile for 5 //passes
check rmdirRemovesOneDir for 5 //counterexample!
check rm_rRemovesSubtree for 5 //counterexample!
check rmAndrm_rSameForFiles for 5 //passes

pred example() {}

run example for exactly 1 FileSystem, exactly 4 FSObject
run example for 2 FileSystem, exactly 3 Dir , exactly 6 File